$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, $a$, $b$:${\it kz}$:Knd$\times$Id fp$\rightarrow$ Top.
\\[0ex]update{-}spec{-}decl($a$;${\it ds}$) $\Rightarrow$ update{-}spec{-}decl($b$;${\it ds}$) $\Rightarrow$ update{-}spec{-}decl($a$ $\oplus$ $b$;${\it ds}$)